$\forall$$T$, $A$:Type, $x$:$T$, ${\it eq}$:EqDecider($T$). AtomFree(Type;$A$) $\Rightarrow$ AtomFree($x$ : $A$)